I think now is a good time to try to address this. At the very least maybe we could add:

-- TODO Morally this is just `isLocalHom_equiv`: can we obviate the need for this instance?
instance (R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
    (e : A ≃ₐ[R] B) : IsLocalHom e.toAlgHom := by
  have : IsLocalHom e.toRingEquiv := inferInstance
  exact ⟨this.map_nonunit⟩

to the appropriate upstream file to shield future users from this awkwardness?

Added the instance, thanks!

I did play around a bit with a proper refactor. One the one hand, it seems that we are moving away from having defs take a FunLike argument (since then you actually get a bunch of different defs). But the issue is that if you switch IsLocalHom to take a plain function, then lemmas that require a ring hom won't fire on compositions (since the lemma will want the coercion of f.comp g, but the available instance will be the function composition of the coercions). So not sure what the best long-term plan is here.